T:Type, L:T List, P1, P2, Q:(||L||Prop), R1, R2:(||L||||L||Prop).
(i:||L||. P1(i)  P2(i))
 (x, y:||L||. R1(x,y)  R2(x,y))
 causal_order(L;R1;P1;Q)
 causal_order(L;R2;P2;Q) 

latex

Definitions	P  Q, x:A. B(x), t  T, ||as||, False, A, AB, P & Q, i  j < k, {i..j}, Prop, x:A. B(x), causal_order(L;R;P;Q)
Lemmas	int seg wf, length wf1, le wf